\def\cprime{$'$}
\begin{thebibliography}{10}

\bibitem{RezkCompletion}
Benedikt Ahrens, Krzysztof Kapulkin, and Michael Shulman.
\newblock Univalent categories and the {R}ezk completion.
\newblock {\em Math. Structures Comput. Sci.}, 25(5):1010--1039, 2015.

\bibitem{Cartmell0}
John Cartmell.
\newblock Generalised algebraic theories and contextual categories.
\newblock {\em Ph.D. Thesis, Oxford University}, 1978.
\newblock \url{https://uf-ias-2012.wikispaces.com/Semantics+of+type+theory}.

\bibitem{Cartmell1}
John Cartmell.
\newblock Generalised algebraic theories and contextual categories.
\newblock {\em Ann. Pure Appl. Logic}, 32(3):209--243, 1986.

\bibitem{FPT}
Marcelo Fiore, Gordon Plotkin, and Daniele Turi.
\newblock Abstract syntax and variable binding (extended abstract).
\newblock In {\em 14th {S}ymposium on {L}ogic in {C}omputer {S}cience
  ({T}rento, 1999)}, pages 193--202. IEEE Computer Soc., Los Alamitos, CA,
  1999.

\bibitem{GabZis}
P.~Gabriel and M.~Zisman.
\newblock {\em Calculus of fractions and homotopy theory}.
\newblock Ergebnisse der Mathematik und ihrer Grenzgebiete, Band 35.
  Springer-Verlag New York, Inc., New York, 1967.

\bibitem{Godement}
Roger Godement.
\newblock {\em Topologie alg\'ebrique et th\'eorie des faisceaux}.
\newblock Actualit'es Sci. Ind. No. 1252. Publ. Math. Univ. Strasbourg. No. 13.
  Hermann, Paris, 1958.

\bibitem{HM2007}
Andr{\'e} Hirschowitz and Marco Maggesi.
\newblock Modules over monads and linearity.
\newblock In {\em Logic, language, information and computation}, volume 4576 of
  {\em Lecture Notes in Comput. Sci.}, pages 218--237. Springer, Berlin, 2007.

\bibitem{HM2008}
Andr{\'e} Hirschowitz and Marco Maggesi.
\newblock Higher order theories.
\newblock {\em \url{http://arxiv.org/abs/0704.2900}}, 2010.

\bibitem{HM2010}
Andr{\'e} Hirschowitz and Marco Maggesi.
\newblock Modules over monads and initial semantics.
\newblock {\em Inform. and Comput.}, 208(5):545--564, 2010.

\bibitem{Jacobs1}
Bart Jacobs.
\newblock {\em Categorical logic and type theory}, volume 141 of {\em Studies
  in Logic and the Foundations of Mathematics}.
\newblock North-Holland Publishing Co., Amsterdam, 1999.

\bibitem{KLV1}
Chris Kapulkin, Peter~LeFanu Lumsdaine, and Vladimir Voevodsky.
\newblock The simplicial model of univalent foundations.
\newblock {\em Available at \url{http://arxiv.org/abs/1211.2851}}, 2012, 2014.

\bibitem{Kleisli}
H.~Kleisli.
\newblock Every standard construction is induced by a pair of adjoint functors.
\newblock {\em Proc. Amer. Math. Soc.}, 16:544--546, 1965.

\bibitem{Lawvere}
F.~William Lawvere.
\newblock Functorial semantics of algebraic theories and some algebraic
  problems in the context of functorial semantics of algebraic theories.
\newblock {\em Repr. Theory Appl. Categ.}, (5):1--121, 2004.
\newblock Reprinted from Proc. Nat. Acad. Sci. U.S.A. {{\bf{5}}0} (1963),
  869--872 [MR0158921] and {{\i}t Reports of the Midwest Category Seminar. II},
  41--61, Springer, Berlin, 1968 [MR0231882].

\bibitem{MacLane}
S.~MacLane.
\newblock {\em Categories for the working mathematician}, volume~5 of {\em
  Graduate texts in {M}athematics}.
\newblock Springer-Verlag, 1971.

\bibitem{Manes}
Ernest~G. Manes.
\newblock {\em Algebraic theories}.
\newblock Springer-Verlag, New York-Heidelberg, 1976.
\newblock Graduate Texts in Mathematics, No. 26.

\bibitem{MLTT79}
Per Martin-L{\"o}f.
\newblock Constructive mathematics and computer programming.
\newblock In {\em Logic, methodology and philosophy of science, {VI}
  ({H}annover, 1979)}, volume 104 of {\em Stud. Logic Found. Math.}, pages
  153--175. North-Holland, Amsterdam, 1982.

\bibitem{Bibliopolis}
Per Martin-L{\"o}f.
\newblock {\em Intuitionistic type theory}, volume~1 of {\em Studies in Proof
  Theory. Lecture Notes}.
\newblock Bibliopolis, Naples, 1984.
\newblock Notes by Giovanni Sambin.

\bibitem{Moggi91}
Eugenio Moggi.
\newblock Notions of computation and monads.
\newblock {\em Inform. and Comput.}, 93(1):55--92, 1991.
\newblock Selections from the 1989 IEEE Symposium on Logic in Computer Science.

\bibitem{Streicher}
Thomas Streicher.
\newblock {\em Semantics of type theory}.
\newblock Progress in Theoretical Computer Science. Birkh\"auser Boston Inc.,
  Boston, MA, 1991.
\newblock Correctness, completeness and independence results, With a foreword
  by Martin Wirsing.

\bibitem{NTS}
Vladimir Voevodsky.
\newblock Notes on type systems.
\newblock {\em \url{https://github.com/vladimirias/old_notes_on_type_systems}},
  2009--2012.

\bibitem{CMUtalk}
Vladimir Voevodsky.
\newblock The equivalence axiom and univalent models of type theory.
\newblock {\em arXiv 1402.5556}, pages 1--11, 2010.

\bibitem{Cfromauniverse}
Vladimir Voevodsky.
\newblock A {C-system} defined by a universe category.
\newblock {\em arXiv 1409.7925, submitted}, pages 1--33, 2015.

\bibitem{UniMath2015}
Vladimir Voevodsky.
\newblock An experimental library of formalized mathematics based on the
  univalent foundations.
\newblock {\em Math. Structures Comput. Sci.}, 25(5):1278--1294, 2015.

\bibitem{fromunivwithpaths}
Vladimir Voevodsky.
\newblock Martin-lof identity types in the c-systems defined by a universe
  category.
\newblock {\em arXiv 1505.06446, submitted}, pages 1--51, 2015.

\bibitem{fromunivwithPi}
Vladimir Voevodsky.
\newblock Products of families of types in the {C-systems} defined by a
  universe category.
\newblock {\em arXiv 1503.07072, submitted}, pages 1--30, 2015.

\bibitem{Csubsystems}
Vladimir Voevodsky.
\newblock Subsystems and regular quotients of {C-systems}.
\newblock In {\em Conference on Mathematics and its Applications, (Kuwait City,
  2014)}, number to appear, pages 1--11, 2015.

\bibitem{UniMath}
Vladimir Voevodsky, Benedikt Ahrens, Daniel Grayson, et~al.
\newblock {\em UniMath}: {Univalent} {Mathematics}.
\newblock Available at \url{https://github.com/UniMath}.

\end{thebibliography}